es{-}when(${\it es}$; $x$; $e$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$es{-}state{-}when(${\it es}$;$e$).$x$